Skip to content

Add contracts for all functions in Alignment #136578

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 6 commits into
base: master
Choose a base branch
from

Conversation

tautschnig
Copy link
Contributor

Uses the contracts syntax introduced in #128045.

@rustbot
Copy link
Collaborator

rustbot commented Feb 5, 2025

Thanks for the pull request, and welcome! The Rust team is excited to review your changes, and you should hear from @tgross35 (or someone else) some time within the next two weeks.

Please see the contribution instructions for more information. Namely, in order to ensure the minimum review times lag, PR authors and assigned reviewers should ensure that the review label (S-waiting-on-review and S-waiting-on-author) stays updated, invoking these commands when appropriate:

  • @rustbot author: the review is finished, PR author should check the comments and take action accordingly
  • @rustbot review: the author is ready for a review, this PR will be queued again in the reviewer's queue

@rustbot rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-libs Relevant to the library team, which will review and decide on the PR/issue. labels Feb 5, 2025
@rust-log-analyzer

This comment has been minimized.

@jieyouxu jieyouxu added the F-contracts `#![feature(contracts)]` label Feb 5, 2025
@jieyouxu
Copy link
Member

jieyouxu commented Feb 5, 2025

You could also tag contracts-related PRs with F-contracts in the future via

@rustbot label: +F-contracts

in a comment / PR description.

@jieyouxu jieyouxu mentioned this pull request Feb 5, 2025
9 tasks
@tgross35
Copy link
Contributor

tgross35 commented Feb 5, 2025

Could you say some more about the motivation? This feature was merged only a number of hours ago, that seems soon to start using in std. Even once it is more stable, what should and shouldn't get contracts is probably something that needs to get discussed.

@rust-lang/libs any thoughts here?

@jieyouxu
Copy link
Member

jieyouxu commented Feb 5, 2025

Yeah, this was only approved as a lang experiment on the lang/compiler side, no idea what the situation is libs side (which certainly should be discussed).

cc @pnkfelix @nikomatsakis @celinval (lang liason and ppl who were implementing this feature compiler side)

@Noratrieb Noratrieb added the I-libs-nominated Nominated for discussion during a libs team meeting. label Feb 5, 2025
@Noratrieb
Copy link
Member

I'll libs nominate this for discussion (this should only be discussed after the contracts people mentioned above have replied).

@celinval
Copy link
Contributor

celinval commented Feb 5, 2025

Totally worth discussion, and it would be great to get some feedback on the features that are needed to meet the libs team bar. I am especially curious to see how you think contracts and ub_checks will interact.

@Noratrieb
Copy link
Member

It would be useful to know what your plan/intention is with adding contracts here. Is it just to try them out or is annotating the standard library with contracts for downstream consumers part of the goal of contracts?

@tautschnig
Copy link
Contributor Author

Could you say some more about the motivation? This feature was merged only a number of hours ago, that seems soon to start using in std. Even once it is more stable, what should and shouldn't get contracts is probably something that needs to get discussed.

As far as the motivation is concerned: we're working towards https://rust-lang.github.io/rust-project-goals/2025h1/std-contracts.html, and I created this (draft) PR with the hope to initiate discussion while knowing there is a lot more work to be done on our end.

As I am new contributor: is there other information that I can provide or another forum that I should use rather than this PR?

@tautschnig
Copy link
Contributor Author

It would be useful to know what your plan/intention is with adding contracts here. Is it just to try them out or is annotating the standard library with contracts for downstream consumers part of the goal of contracts?

Our current goal is https://rust-lang.github.io/rust-project-goals/2025h1/std-contracts.html, though we are in early stages and it indeed is about trying out what works best. Eventually we want to enable verification of downstream consumers, but a lot more work will be required before we get there.

@tautschnig tautschnig force-pushed the upstream-contracts/alignment branch from d46f868 to 7288286 Compare February 5, 2025 22:06
@rust-log-analyzer

This comment has been minimized.

@tgross35
Copy link
Contributor

tgross35 commented Feb 5, 2025

As far as the motivation is concerned: we're working towards https://rust-lang.github.io/rust-project-goals/2025h1/std-contracts.html, and I created this (draft) PR with the hope to initiate discussion while knowing there is a lot more work to be done on our end.

As I am new contributor: is there other information that I can provide or another forum that I should use rather than this PR?

Are there any docs on how contracts work as they exist today? Ignoring the stability question, we need something to refer to about how to use these properly, e.g. in https://doc.rust-lang.org/nightly/unstable-book/. Also, how are contracts that get merged into r-l/rust being verified?

The linked page is somewhat vague about what this means for std. I think we could also use a policy page in the library dev guide (https://std-dev-guide.rust-lang.org) giving guidelines for their use, based on the outcome of any discussion that happens.

Bringing this up on the libs zulip would be a good idea to get the ball rolling https://rust-lang.zulipchat.com/#narrow/channel/219381-t-libs.

@@ -43,6 +43,8 @@ impl Alignment {
#[unstable(feature = "ptr_alignment_type", issue = "102070")]
#[inline]
#[must_use]
#[cfg_attr(not(bootstrap), contracts::requires(mem::align_of::<T>().is_power_of_two()))]

This comment was marked as resolved.

@tautschnig tautschnig force-pushed the upstream-contracts/alignment branch from 7288286 to c180bd0 Compare February 6, 2025 13:23
@rust-log-analyzer

This comment has been minimized.

@rust-log-analyzer

This comment has been minimized.

@Amanieu
Copy link
Member

Amanieu commented Feb 12, 2025

We discussed this in the libs meeting today. We're happy to add contracts to the standard library as an experiment, as long as this doesn't get in the way of normal standard library development. Depending on how the contracts feature evolves, we may reconsider our level of support.

@Amanieu Amanieu removed the I-libs-nominated Nominated for discussion during a libs team meeting. label Feb 12, 2025
@tautschnig

This comment was marked as outdated.

@RalfJung
Copy link
Member

What is the difference you are seeing?

@tautschnig

This comment was marked as outdated.

@bors
Copy link
Collaborator

bors commented May 13, 2025

☔ The latest upstream changes (presumably #140887) made this pull request unmergeable. Please resolve the merge conflicts.

@Dylan-DPC
Copy link
Member

@tautschnig any updates on this? thanks

@tautschnig tautschnig force-pushed the upstream-contracts/alignment branch from bef04bf to 37e0b32 Compare August 20, 2025 21:05
@rust-log-analyzer

This comment has been minimized.

tautschnig added a commit to tautschnig/verify-rust-std that referenced this pull request Aug 21, 2025
@tautschnig tautschnig force-pushed the upstream-contracts/alignment branch 2 times, most recently from bad50a8 to 3402194 Compare August 21, 2025 10:20
tautschnig added a commit to tautschnig/verify-rust-std that referenced this pull request Aug 21, 2025
@tautschnig tautschnig marked this pull request as ready for review August 21, 2025 10:22
@rustbot rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. and removed S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. labels Aug 21, 2025
@rustbot
Copy link
Collaborator

rustbot commented Aug 21, 2025

The Miri subtree was changed

cc @rust-lang/miri

Some changes occurred to the intrinsics. Make sure the CTFE / Miri interpreter
gets adapted for the changes, if necessary.

cc @rust-lang/miri, @RalfJung, @oli-obk, @lcnr

@rustbot

This comment has been minimized.

Uses the experimental contracts syntax..
Contracts can affect 1) whether we get a constant and 2) which value we
are moving.
Updated via `./x.py test mir-opt --bless --stage 1` plus a manual tweak
of `tests/mir-opt/gvn_ptr_eq_with_constant.main.GVN.diff`.
Contracts result in function calls that would make the inlining test
spuriously fail.
@tautschnig tautschnig force-pushed the upstream-contracts/alignment branch from 3402194 to 23fefad Compare August 21, 2025 10:24
pub fn leaf_fn() -> String {
String::new()
pub fn leaf_fn() -> bool {
Some(0).is_some()

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this the way we want to handle the test failure? Surely, we don't want contracts to affect the inlining?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, I think UB checks already do.

IMO the important case is that trivial getters and setters that literally only do a field access get made cross-crate-inlineable. Also managing to detect functions that optimize to just a load or store is gravy. It's impossible in the general case, because of the limitations of the current compilation model and query system. And it's sometimes undesirable because making a function cross-crate-inlineable increases the amount of code that dependent crates need to compile, which can regress incremental build times.

... Wouldn't hurt to have that sort of explanation in the codebase.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In addition, I think there's a possible future extension to the cross-crate-inlineable analysis that excludes code underneath a UB check or contract check from the cost model.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe disabled contracts should have zero runtime penalties, since they serve a different purpose to UB checks or any other form of existing runtime assertion. Their role is more akin to doctests: documentation that can be executed for testing purposes. Additionally contracts are a means to facilitate formal verification.

These are the goals of contracts stated by the draft RFC.

  1. They form precise, machine readable documentation of the expected behaviour of your code.
  2. They can be automatically converted into assert! checks, and then validated using your existing unit, property, fuzz, and integration tests.
  3. They form the specification for formal verification tools. In cases where these tools can prove the absence of bugs, the checks can be elided entirely from the code, giving you safety with no runtime cost. These formally verified checks can even form the basis of assume statements, enabling additional optimization within the compiler (e.g. allowing the compiler to remove bounds checks on accesses that can be formally proven to be safe).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure you understood what I was saying, so I'm rephrasing. UB checks currently have an impact on optimizations (that look exactly like the diff we are commenting on) even when they are completely disabled at runtime. In an ideal world, they wouldn't. But the actual consequences here are very minimal in practice, so we haven't yet invested very heavily in making the compiler perfect.

Copy link
Member

@RalfJung RalfJung Aug 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For some reason it's not able to constant propagate the None so that contract_check_requires(__postcond, body) expands to just body.

contract_check_requires has signature fn contract_check_requires<C: Fn() -> bool + Copy>(cond: C) so I can't match that up with the code you are posting here. Do you mean contract_check_ensures? But there's no Option argument there either...

But anyway it seems you want contract_check_ensures to be inlined but intrinsics do not get inlined since backends may want to plug in their own implementation. This may need a custom optimization pass. Right now though it's unclear to me why this is an intrinsic in the first place, and your example code doesn't match the actual signatures, so what this needs most is a step back and a plan -- blind experimentation isn't going to get us there.

Copy link

@dawidl022 dawidl022 Aug 23, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, sorry, I meant contract_check_ensures (edited my previous comment now). I'm referring to my code in #144438, which @celinval linked to.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah... please don't spread the discussion over multiple PRs, that will be impossible to follow.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably best to mark this PR here as a draft and suspend it until #144438 is done.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

if there was even a slight possibility of runtime penalties.

I think this is an unreasonable criteria, and I tried to explain why by referring to the if T::IS_ZST pattern.

@@ -2605,6 +2605,7 @@ pub const fn contract_checks() -> bool {
// doesn't honor `#[allow_internal_unstable]`, so for the const feature gate we use the user-facing
// `contracts` feature rather than the perma-unstable `contracts_internals`
#[rustc_const_unstable(feature = "contracts", issue = "128044")]
#[miri::intrinsic_fallback_is_spec]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems that no backend actually overwrites this intrinsic. Why is it an intrinsic in the first place...? (Same for contract_check_ensures.)

@RalfJung RalfJung added S-blocked Status: Blocked on something else such as an RFC or other implementation work. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Aug 23, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
F-contracts `#![feature(contracts)]` S-blocked Status: Blocked on something else such as an RFC or other implementation work. T-libs Relevant to the library team, which will review and decide on the PR/issue.
Projects
None yet
Development

Successfully merging this pull request may close these issues.